1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
use super::*;

/// A relationship between relations
#[derive(Copy, Clone, Eq, PartialEq, Hash)]
pub struct Relationship {
    /// The variance of this relationship
    variance: Variance,
    /// Whether this relationship is strict
    strict: bool,
    /// The usage of this relationship
    usage: Usage,
}

impl PartialOrd for Relationship {
    #[inline]
    fn partial_cmp(&self, other: &Relationship) -> Option<Ordering> {
        self.const_cmp(*other)
    }
}

impl Relationship {
    /// One instant is before another
    pub const LE: Relationship = Relationship {
        variance: Contravariant,
        strict: false,
        usage: Usage::UNUSED,
    };
    /// One instant is after another
    pub const GE: Relationship = Relationship {
        variance: Covariant,
        strict: false,
        usage: Usage::UNUSED,
    };
    /// One instant is *strictly* before another
    pub const LT: Relationship = Relationship {
        variance: Contravariant,
        strict: true,
        usage: Usage::UNUSED,
    };
    /// One instant is *strictly* after another
    pub const GT: Relationship = Relationship {
        variance: Covariant,
        strict: true,
        usage: Usage::UNUSED,
    };
    /// One instant is equal to another
    pub const EQ: Relationship = Relationship {
        variance: Invariant,
        strict: false,
        usage: Usage::UNUSED,
    };
    /// One instant is distinct from another, with no particular ordering
    pub const NE: Relationship = Relationship {
        variance: Bivariant,
        strict: true,
        usage: Usage::UNUSED,
    };
    /// One instant is both strictly before and strictly after another: an impossibility
    pub const CN: Relationship = Relationship {
        variance: Invariant,
        strict: true,
        usage: Usage::OBSERVED,
    };
    /// One instant is either before or after another, not excluding equality.
    pub const TV: Relationship = Relationship {
        variance: Bivariant,
        strict: false,
        usage: Usage::CONSUMED,
    };
    /// Make this relationship into a strict one
    #[inline]
    pub const fn into_strict(self) -> Relationship {
        Relationship {
            strict: true,
            ..self
        }
        .normalize()
    }
    /// Get this relationship with a given usage
    #[inline]
    pub const fn with_usage(self, usage: Usage) -> Relationship {
        Relationship { usage, ..self }.normalize()
    }
    /// Get the relationship with a dependency having a given Usage
    #[inline]
    pub const fn dependency(usage: Usage) -> Relationship {
        Relationship::GE.with_usage(usage)
    }
    /// Multiply a relationship by another's time direction
    #[inline]
    pub const fn multiply_time(self, time: Relationship) -> Relationship {
        Relationship {
            variance: self.variance.multiply(time.variance),
            strict: self.strict | time.strict,
            usage: self.usage.meet(time.usage),
        }
    }
    /// Flip a relationship
    #[inline]
    pub const fn flip(self) -> Relationship {
        Relationship {
            variance: self.variance.flip(),
            ..self
        }
    }
    /// Take the supremum of two relationships
    #[inline]
    pub const fn join(self, other: Relationship) -> Relationship {
        Relationship {
            variance: self.variance.meet(other.variance),
            strict: self.strict & other.strict,
            usage: self.usage.join(other.usage),
        }
        .normalize()
    }
    /// Take the supremum of a relationship and a usage
    #[inline]
    pub const fn join_usage(self, other: Usage) -> Relationship {
        Relationship {
            usage: self.usage.join(other),
            ..self
        }
        .normalize()
    }
    /// Take the infimum of two relationships
    #[inline]
    pub const fn meet(self, other: Relationship) -> Relationship {
        Relationship {
            variance: self.variance.join(other.variance),
            strict: self.strict | other.strict,
            usage: self.usage.meet(other.usage),
        }
        .normalize()
    }
    /// Take the infimum of a relationship and a usage
    #[inline]
    pub const fn meet_usage(self, other: Usage) -> Relationship {
        Relationship {
            usage: self.usage.meet(other),
            ..self
        }
        .normalize()
    }
    /// Take the conjunction of a relationship and a usage
    #[inline]
    pub const fn conj_usage(self, other: Usage) -> Relationship {
        Relationship {
            usage: self.usage.conj(other),
            ..self
        }
        .normalize()
    }
    /// Take the separating conjunction of a relationship and a usage
    #[inline]
    pub const fn sep_conj_usage(self, other: Usage) -> Relationship {
        let usage = if let Ok(usage) = self.usage.sep_conj(other) {
            usage
        } else {
            return Relationship::CN;
        };
        Relationship { usage, ..self }.normalize()
    }
    /// Take the separating conjunction of two relationships
    #[inline]
    pub const fn sep_conj(self, other: Relationship) -> Relationship {
        let usage = if let Ok(usage) = self.usage.sep_conj(other.usage) {
            usage
        } else {
            return Relationship::CN;
        };
        Relationship {
            usage,
            strict: self.strict | other.strict,
            variance: self.variance.join(other.variance),
        }
        .normalize()
    }
    /// Unify contradictions. Should be a no-op for constructable `Relationship`s
    #[inline]
    const fn normalize(self) -> Relationship {
        if self.is_contradiction() {
            Self::CN
        } else if self.is_trivial() {
            self::TV
        } else {
            self
        }
    }
    /// Check whether this relationship would imply a contradiction, i.e. is always false
    #[inline]
    pub const fn is_contradiction(self) -> bool {
        matches!(self.variance, Invariant) && self.strict
    }
    /// Check whether this relationship is trivial, i.e. is always true
    #[inline]
    pub const fn is_trivial(self) -> bool {
        matches!(self.variance, Bivariant) && !self.strict
    }
    /// Get the variance of this relationship
    #[inline]
    pub const fn variance(self) -> Variance {
        self.variance
    }
    /// Get whether this relationship is strict
    #[inline]
    pub const fn strict(self) -> bool {
        self.strict
    }
    /// Get the usage of this relationship
    #[inline]
    pub const fn usage(self) -> Usage {
        self.usage
    }
    /// Get the directed usage of this relationship
    #[inline]
    pub const fn directed_usage(self, direction: Variance) -> Usage {
        use Ordering::*;
        if matches!(direction.const_cmp(self.variance), Some(Less) | Some(Equal)) {
            self.usage
        } else {
            Usage::UNUSED
        }
    }
    /// Get the usage of this relationship with respect to a dependency
    #[inline]
    pub const fn dependent_usage(self) -> Usage {
        self.directed_usage(Variance::Covariant)
    }
    /// Get whether this relationship is pure
    #[inline]
    pub const fn is_pure(self) -> bool {
        self.is_contradiction() || self.usage.const_eq(Usage::UNUSED)
    }
    /// Get this relationship as a pure relationship
    #[inline]
    pub const fn into_pure(self) -> Relationship {
        self.with_usage(Usage::UNUSED)
    }
    /// Take a given relationship, with respect to a given symbol
    #[inline]
    pub fn of(self, symbol: &SymbolId) -> Relationship {
        self.join_usage(symbol.ty().elem_linearity().unwrap().max_usage())
    }
    /// Get a string representation of this relationship
    #[inline]
    pub const fn into_str(self) -> &'static str {
        const OBSERVED: Usage = Usage::OBSERVED;
        const CONSUMED: Usage = Usage::CONSUMED;
        const UNUSED: Usage = Usage::UNUSED;
        const USED: Usage = Usage::USED;
        match (self.variance, self.usage, self.strict) {
            (Contravariant, OBSERVED, false) => "(<=)[Observed]",
            (Contravariant, CONSUMED, false) => "(<=)[Consumed]",
            (Contravariant, UNUSED, false) => "(<=)",
            (Contravariant, USED, false) => "(<=)[Used]",
            (Covariant, OBSERVED, false) => "(>=)[Observed]",
            (Covariant, CONSUMED, false) => "(>=)[Consumed]",
            (Covariant, UNUSED, false) => "(>=)",
            (Covariant, USED, false) => "(>=)[Used]",
            (Contravariant, OBSERVED, true) => "(<)[Observed]",
            (Contravariant, CONSUMED, true) => "(<)[Consumed]",
            (Contravariant, UNUSED, true) => "(<)",
            (Contravariant, USED, true) => "(<)[Used]",
            (Covariant, OBSERVED, true) => "(>)[Observed]",
            (Covariant, CONSUMED, true) => "(>)[Consumed]",
            (Covariant, UNUSED, true) => "(>)",
            (Covariant, USED, true) => "(>)[Used]",
            (Invariant, OBSERVED, false) => "(==)[Observed]",
            (Invariant, CONSUMED, false) => "(==)[Consumed]",
            (Invariant, UNUSED, false) => "(==)",
            (Invariant, USED, false) => "(==)[Used]",
            (Bivariant, OBSERVED, true) => "(!=)[Observed]",
            (Bivariant, CONSUMED, true) => "(!=)[Consumed]",
            (Bivariant, UNUSED, true) => "(!=)",
            (Bivariant, USED, true) => "(!=)[Used]",
            (Invariant, OBSERVED, true) => "!",
            (Bivariant, CONSUMED, false) => "*",
            _ => "bad",
        }
    }
    /// Take the constant comparison of two relationships
    #[inline]
    pub const fn const_cmp(self, other: Relationship) -> Option<Ordering> {
        //#[allow(clippy::manual_map)]
        let variance_cmp = if let Some(variance) = self.variance.const_cmp(other.variance) {
            Some(variance.reverse())
        } else {
            None
        };
        let usage_cmp = self.usage.const_cmp(other.usage);
        let variance_usage_cmp = lattice_ord_opt(variance_cmp, usage_cmp);
        let strict_cmp = bool_cmp(self.strict, other.strict).reverse();
        lattice_ord_opt(variance_usage_cmp, Some(strict_cmp))
    }
    /// Get the code of this relationship
    #[inline]
    pub const fn code(self) -> u64 {
        self.variance.code() | self.usage.code() | ((self.strict as u64) << 4)
    }
}

impl Debug for Relationship {
    fn fmt(&self, fmt: &mut Formatter) -> fmt::Result {
        fmt::Display::fmt(self.into_str(), fmt)
    }
}

impl BitAnd for Relationship {
    type Output = Relationship;
    fn bitand(self, other: Relationship) -> Relationship {
        self.meet(other)
    }
}

impl BitOr for Relationship {
    type Output = Relationship;
    fn bitor(self, other: Relationship) -> Relationship {
        self.join(other)
    }
}

impl Mul for Relationship {
    type Output = Relationship;
    fn mul(self, other: Relationship) -> Relationship {
        self.sep_conj(other)
    }
}

/// Relationships between instants
pub mod relationships {
    pub use super::Relationship;
    /// One instant is before another
    pub const LE: Relationship = Relationship::LE;
    /// One instant is after another
    pub const GE: Relationship = Relationship::GE;
    /// One instant is *strictly* before another
    pub const LT: Relationship = Relationship::LT;
    /// One instant is *strictly* after another
    pub const GT: Relationship = Relationship::GT;
    /// One instant is not equal to another
    pub const NE: Relationship = Relationship::NE;
    /// One instant is equal to another
    pub const EQ: Relationship = Relationship::EQ;
    /// Always false
    pub const CN: Relationship = Relationship::CN;
    /// Always true, inducing a false dependency between instants
    pub const TV: Relationship = Relationship::TV;
}
use relationships::*;

/// Basic relationships
pub const BASIC_RELATIONSHIPS: [Relationship; 8] = [LE, GE, LT, GT, NE, EQ, CN, TV];
/// All relationships
pub const RELATIONSHIPS: [Relationship; 32] = [
    LE.with_usage(Usage::OBSERVED),
    GE.with_usage(Usage::OBSERVED),
    LT.with_usage(Usage::OBSERVED),
    GT.with_usage(Usage::OBSERVED),
    NE.with_usage(Usage::OBSERVED),
    EQ.with_usage(Usage::OBSERVED),
    CN.with_usage(Usage::OBSERVED),
    TV.with_usage(Usage::OBSERVED),
    LE.with_usage(Usage::CONSUMED),
    GE.with_usage(Usage::CONSUMED),
    LT.with_usage(Usage::CONSUMED),
    GT.with_usage(Usage::CONSUMED),
    NE.with_usage(Usage::CONSUMED),
    EQ.with_usage(Usage::CONSUMED),
    CN.with_usage(Usage::CONSUMED),
    TV.with_usage(Usage::CONSUMED),
    LE.with_usage(Usage::UNUSED),
    GE.with_usage(Usage::UNUSED),
    LT.with_usage(Usage::UNUSED),
    GT.with_usage(Usage::UNUSED),
    NE.with_usage(Usage::UNUSED),
    EQ.with_usage(Usage::UNUSED),
    CN.with_usage(Usage::UNUSED),
    TV.with_usage(Usage::UNUSED),
    LE.with_usage(Usage::USED),
    GE.with_usage(Usage::USED),
    LT.with_usage(Usage::USED),
    GT.with_usage(Usage::USED),
    NE.with_usage(Usage::USED),
    EQ.with_usage(Usage::USED),
    CN.with_usage(Usage::USED),
    TV.with_usage(Usage::USED),
];

#[cfg(test)]
mod test {
    use super::*;
    #[test]
    fn flip() {
        let flipped = [(GE, LE), (GT, LT), (EQ, EQ), (NE, NE), (CN, CN), (TV, TV)];
        for &(left, right) in flipped.iter() {
            assert_eq!(left.flip(), right);
            assert_eq!(right.flip(), left);
        }
    }
    #[test]
    fn partial_ord() {
        for &left in &RELATIONSHIPS {
            assert!(CN <= left, "{:?} <= {:?}", CN, left);
            assert!(TV >= left, "{:?} >= {:?}", TV, left);
            for &right in &RELATIONSHIPS {
                assert!(
                    left.meet(right) <= left,
                    "{:?} & {:?} = {:?} <= {:?}",
                    left,
                    right,
                    left.meet(right),
                    left
                );
                assert!(
                    left.join(right) >= left,
                    "{:?} | {:?} = {:?} >= {:?}",
                    left,
                    right,
                    left.join(right),
                    left
                );
            }
        }
    }
    #[test]
    fn dependent_usage() {
        assert_eq!(TV.dependent_usage(), Usage::UNUSED)
    }
    #[test]
    fn meet_join_sep() {
        let tuples = [
            // GE
            (GE, GE, GE, GE, GE),
            (GE, LE, EQ, TV, EQ),
            (GE, GT, GT, GE, GT),
            (GE, LT, CN, TV, CN),
            (GE, EQ, EQ, GE, EQ),
            (GE, NE, GT, TV, GT),
            (GE, CN, CN, GE, CN),
            (GE, TV, GE, TV, GE),
            // LE
            (LE, LE, LE, LE, LE),
            (LE, GT, CN, TV, CN),
            (LE, LT, LT, LE, LT),
            (LE, EQ, EQ, LE, EQ),
            (LE, NE, LT, TV, LT),
            (LE, CN, CN, LE, CN),
            (LE, TV, LE, TV, LE),
            // GT
            (GT, GT, GT, GT, GT),
            (GT, LT, CN, NE, CN),
            (GT, EQ, CN, GE, CN),
            (GT, NE, GT, NE, GT),
            (GT, CN, CN, GT, CN),
            (GT, TV, GT, TV, GT),
            // LT
            (LT, LT, LT, LT, LT),
            (LT, EQ, CN, LE, CN),
            (LT, NE, LT, NE, LT),
            (LT, CN, CN, LT, CN),
            (LT, TV, LT, TV, LT),
            // EQ
            (EQ, EQ, EQ, EQ, EQ),
            (EQ, NE, CN, TV, CN),
            (EQ, CN, CN, EQ, CN),
            (EQ, TV, EQ, TV, EQ),
            // NE
            (NE, NE, NE, NE, NE),
            (NE, CN, CN, NE, CN),
            (NE, TV, NE, TV, NE),
            // CN
            (CN, CN, CN, CN, CN),
            (CN, TV, CN, TV, CN),
            // TV
            (TV, TV, TV, TV, TV),
        ];
        for &(left, right, meet, join, sep) in tuples.iter() {
            for &left_usage in &Usage::USAGES {
                for &right_usage in &Usage::USAGES {
                    let left = left.with_usage(left_usage);
                    let right = right.with_usage(right_usage);
                    let left_usage = left.usage();
                    let right_usage = right.usage();
                    let meet = meet.with_usage(left_usage.meet(right_usage));
                    let join = join.with_usage(left_usage.join(right_usage));
                    let sep = left_usage
                        .sep_conj(right_usage)
                        .map(|usage| sep.with_usage(usage))
                        .unwrap_or(Relationship::CN);
                    assert_eq!(left & right, meet, "{:?} & {:?} == {:?}", left, right, meet);
                    assert_eq!(right & left, meet, "{:?} & {:?} == {:?}", right, left, meet);
                    assert_eq!(left | right, join, "{:?} | {:?} == {:?}", left, right, join);
                    assert_eq!(right | left, join, "{:?} | {:?} == {:?}", right, left, join);
                    assert_eq!(left * right, sep, "{:?} * {:?} == {:?}", left, right, sep);
                    assert_eq!(right * left, sep, "{:?} * {:?} == {:?}", right, left, sep);
                }
            }
        }
    }
}